Summary

• Adds measureDseCorrectness flag: after Z3 returns SAT, the generated rows are fed back through SqlHeuristicsCalculator to compute a distance to the original SQL predicate — logs a warning if
  distance is non-zero and records it in Statistics
• Fixes composite primary key handling in SmtLibGenerator: the old code required every PK column to differ individually across rows, which was over-constrained (e.g. it ruled out (emp=1, proj=2) and (emp=1, proj=3) as a pair). Now emits an OR assertion so only the tuple must be distinct
• Extends SmtLibGenerator to handle DELETE and UPDATE statements, not just SELECT
• Fixes LongValue gene mapping: was calling .toInt() and silently truncating large values; now uses LongGene
• Adds JSqlVisitor parsing improvements and new SmtLibGeneratorTest coverage

Motivation

The Z3 solver could generate rows that technically satisfy the SMT-LIB encoding but fail the original SQL predicate, due to encoding gaps (composite PKs, unsupported statement types, type
truncation). This PR adds a post-hoc verification step to detect those cases and tracks them as a metric, while also fixing the most common encoding bugs that caused them.

New Stats